Formal Methods for the Analysis of Security Protocols (supervised by Paulo Mateus and Andre Scedrov)
PhD Thesis, IST, Universidade Técnica de Lisboa, June 2006.

Abstract: As Computational Cryptography is hard to deal manually, several abstractions have been proposed to analyse security protocols, being one of the most successful the Dolev-Yao abstraction. However, one should investigate how reliable are such abstractions, hence the need to relate these two approaches. In this dissertation we start by considering the original Abadi-Rogaway logic of formal encryption and its soundness result, observing then that this result has two weaknesses. The first is that it cannot tolerate key-cycles, and the second is that the assumption of length-concealing encryption scheme is too strong. We fix both these problems, the former strengthening the computational model, and the latter by considering a more general class of logics. The second contribution of this dissertation is the proposal of a language that is variant of the pi-calculus with secure communications, mobile names, and high-level certificates, but with no explicit cryptography. Within this language, security properties can be conveniently studied using trace properties and observational equivalence in the presence of active adversaries. We provide a concrete implementation that is both sound and complete with respect to computational cryptography. Finally, and arguably one step ahead of reality, we introduce a language also similar to the pi-calculus, that enable us to express and study security properties of quantum cryptographic protocols.

Category / Keywords. Cryptography, Key-Cycles, Process Calculi, Quantum Security, Security, Sound Abstractions of Formal Cryptography.

Publication Info. PhD Thesis.

Date: 6 June 2006.

Get a preprint: PDF | PS | BibTeX Citation.